$\forall$$T$:Type, $P$:($i$:Id$\rightarrow$\{$k$:Knd$\mid$ $\uparrow$hasloc($k$;$i$)\} $\rightarrow$$T$), ${\it ik}$:LocKnd. let $i$,$k$:LocKnd = ${\it ik}$ in $P$($i$,$k$) $\in$ $T$